value restriction

#型システム

問題

非純粋･call by value･多相の3つが揃うとき大変なことが起こる｡

今､value restrictionのないML方言と参照セルとリストコンストラクタを用意する｡let多相があると､let-boundなものを多相にすることができる｡

code:ocaml

let r : 'a list ref = ref [] in

......

rは多相なリスト'a listを持っているので'a list ref 型になる｡さて､rのリストの参照を更新していくわけだが

code:ocaml

r := "hello" :: !r;

r := "world" :: !r;

!r では string list ref に型が特殊化されるが､ := 左辺の rは依然として'a list ref型である｡つまり…

code:ocaml

r := true :: !r; (* エッ?! *)

このコードは型システムによって咎められない｡というのも右辺のrは利用されるまでは'a list ref型であり､!rで初めてbool list refになる｡したがってこの参照セルの中身は[true; "world"; "hello"] となり､型エラーがランタイムに発生する可能性がある｡

弱い多相たそ

このように､型システムがあっても健全性が失われる悲しい事態を避けるために､弱い多相を入れる｡

code:ocaml

let r : '_a list ref = ref [] in

......

'_a は一見してただの型変数だが､一度特殊化されるとソレ以降ずっと特殊化された(つまり単相な)型になる｡

code:ocaml

r := "hello" :: !r;

(* ==> val r : _string_ list ref *)

したがって次のようなコードが続くと静的に型エラーで弾くことができる｡

code:ocaml

r := true :: !r; (* Error: This expression has type bool but なんとかかんとか､つまりダメ *)

問題2

しかし何でもかんでも弱い多相にすると大変困る｡よくある例としてid関数を見てみる｡

code:ocaml

let id : '_a -> '_a ...? = fun x -> x

コレが弱い多相になっちまうってぇと…

code:ocaml

let s = id "string" in (* ==> id : string -> string (x_x) *)

let i = id 3 in (* Error: This expression has type int but idはstring -> stringだよ〜ん *)

......

まあ､とにかくダメですね｡

relaxed value restriction

ML､もう全部単相か…というお通夜ムードに対し､Jacques Garrigue氏が打開策を出した｡

簡単に述べると､letで束縛される値(リテラル)の型変数､または式の型のcovariant positionに現れる型変数は多相性を回復して良いというものである｡

covariant positionとは､あまり理解してないけど､ -> の右辺のことである｡

code:ocaml

(* fun x -> x というリテラルに相当するので 'a -> 'a *)

let id x = x

(* リテラルではない､かつ (('a -> 'b) -> 'a list -> 'b list) にある型'_aに特殊化されたid:'_a -> '_aが適用されるので *)

(** '_a list -> '_a list *)

let map_id = List.map id

(* fun l -> List.map id l というリテラルに相当し､ '_a -> '_a から多相性を回復して 'a -> 'a *)

let map_id' l = List.map id l

特に最後の例は､map_id の定義をeta conversionしたものと考えることができる｡

TypeScriptに関する残念なお知らせ

弊社でも利用しているTypeScriptは､var または let で定義した変数への代入を許している(varは使うなマジで)｡

code:typescript

const × = 3;

x = 2; // 構文エラー

let y = 5;

y = 8; // OK

TSにおいて型変数は関数でしか利用できない｡ところでany は考えないものとする｡

code:typescript

let t = []; // 型変数を許さない(しanyなんて信じない)のでArray<なんとか>になる

t = 3, ...t; // 型推論が働いてくれればtは Array<number>になる

t = "aa", ...t; // なので無事型エラー

call by value､多相のTypeScriptには参照セルがないので問題なかった｡

…わけではない｡こちらをご覧ください｡https://github.com/microsoft/TypeScript/issues/31152

TypeScriptにおいては､Objectを参照セルとして扱うことができる｡これを利用すると､簡単に型エラーをランタイムに発生させることができる｡上記で問題となるコードを少し変えて見てみる｡

code:typescript

function ref<T>(f: (x: T) => T): () => { val: (x: T) => T } {

const r = {val : f};

return () => r;

};

const id = <T>(x: T) => x;

const r = ref(id);

const r1 = r<number>();

const r2 = r<string>();

r1.val = (x: number) => x + 1;

console.log(r2.val("ok") === "ok"); // ==> false

console.log(r2.val("ok") === "ok1"); // ==> true (!)

rがクロージングしているオブジェクトをr1とr2が共有してしまっている｡したがってr1.val に関数を代入するとr2.val でも同じ関数を指すことになる｡なのでr2.val("ok")とすると"ok" + 1 の結果が出てくるようになる｡幸い(?)なことに二項演算子+はnumber => string => string をオーバーロードしている(嘘)ので型エラーこそ起こらないが全く意味不明な文字列"ok1"が生成され､バグの温床となることは容易に想像できる｡多相なオブジェクトには細心の注意を払う必要がある｡

この問題は､tsc 3.5.3で確認した｡

Reference

Garrigue, Jacques. "Relaxing the value restriction." International Symposium on Functional and Logic Programming. Springer, Berlin, Heidelberg, 2004.